REF, NoConds
(a THENA b) == ((a) CollapseTHENA (b)) 

latex

---

clarification:

REF, NoConds
(a THENA b) == ((a) CollapseTHENA (b)) 

latex

Up	Tactics as terms
FDL editor aliases	-tha